Quint LLM kit

Informal Systems製のQuintをLLMと組み合わせて使うためのエージェント・ツールキット

Apache-2.0ライセンス、現在5 stars、Bluespec/Rust/TypeScript/TLA混在のリポジトリ

Quintとは(背景)

QuintはInformal Systemsが開発する形式仕様記述言語、TLA+系の流れにある現代的なformal spec

詳細はブログ記事Reliable Software in the LLM Eraに背景思想がまとまっている

このリポジトリの位置付け

元々はInformal Systems社内実験用に開発された

ブログ記事の実験で使われたツール群を公開したもの

「社内利用前提でテスト不十分」と明記されたディスクレーマ付き、自己責任での利用を前提

コラボレーション歓迎、Issueやフィードバックを募集中

提供物 (Dockerコンテナ)

Claude Code CLIがプリインストールされた開発環境

Quint向け特化エージェント: analyzer / implementer / verifier など

MCPサーバ: Quintドキュメント(quint-kb)とLSP連携(quint-lsp)

共通開発ツール: Go 1.24.1、Python 3、Rust(rustup)、Node.js 20.x、git/curl/jq/tree

オプションでFoundry(Solidity開発ツールチェーン)を含めることも可能

セキュリティ目的で非rootユーザ(dev)で実行される

主要な使い方

make buildでDockerイメージclaudecode:latestをビルド

make run DIR=~/my-projectでプロジェクトをマウントして起動

make run単体で対話的にパスを聞かれる起動も可能

MCPサーバ(quint-lsp・quint-kb)は初回起動時に自動設定される

APIキーはイメージやホストではなくコンテナ内Claude Codeに保管される

make stopでコンテナを片付ける

Claude commands

/mine:nextを実行すると次に試せそうなことを提案してくれる

Quint仕様がまだプロジェクトにない初期状態からでも使える

困ったらまず/mine:next、というワークフロー設計

構造

agentic/: 各種エージェント定義

mcp-servers/: MCPサーバ実装

claudecode.dockerfile、entrypoint.sh、code.sh、setup-mcp.sh、Makefileが起動・セットアップを担当

.mcp.json.exampleがMCP設定のテンプレート

FOUNDRY.mdがSolidity連携の追加手順

想定される使いどころ

LLMに形式仕様を書かせる/レビューさせる実験

Claude Codeを中心にアナライザ・実装者・検証者の役割を分担させる多エージェントワークフロー

Quint初心者がClaudeに手助けされながら仕様を書き始めるオンランプ